module TravelDream
open util/integer as intop

//---------------------------------------------------------
//        DEFINIZIONE TIPI DI DATO
//---------------------------------------------------------

sig Stringa{}
sig Intero{}
sig Citta{}

//---------------------------------------------------------
//        DEFINIZIONE ENTITA'
//---------------------------------------------------------

// Entità data
sig Data{
	anno: one Intero,
	mese: one Intero,
	giorno: one Intero,
	ora: one Intero,
	minuto: one Intero,
	timestamp: Int
} {
	timestamp > 0
}

sig PacchettoPreconfigurato {
	nome: one Stringa,
	descrizione: one Stringa,
	destinazione: one Citta,
	durata: Int,
	prezzoPack: one Intero,
	
	viaggiAndataCompat: some Trasporto,
	viaggiRitornoCompat: some Trasporto,
	soggiorniCompat: some Soggiorno,
	datePartenzaPossibili: some Data,
	attivitaOpzCompat: some Attivita,
	attivitaObblig: set Attivita
} {
	 // La durata di una vacanza è positiva
	durata > 0

	// Viaggi e soggiorni compatibili sono solo quelli relativi alla destinazione pubblicizzata 
	// dal pacchetto
	all t : Trasporto | t in viaggiAndataCompat <=> t.cittaArrivo = destinazione
	all t : Trasporto | t in viaggiRitornoCompat <=> t.cittaPartenza = destinazione
	all s : Soggiorno | s in soggiorniCompat <=> s.citta = destinazione

	// Le attività in attivitaOpzCompat sono attività compatibili con il pacchetto 
	// preconfigurato a cui appartengono, che non siano già inserite come obbligatorie
	all a : Attivita | a in attivitaOpzCompat implies (
		a.cittaFruiz = destinazione and a not in attivitaObblig and
		some dp : Data | dp in datePartenzaPossibili and 
			a.dataInizioDisp.timestamp <= dp.timestamp and
			a.dataFineDisp.timestamp >= dp.timestamp+durata
	)

	// Le attività inserite dall'impiegato hanno gli stessi vincoli delle attività compatibili.
	// I due insiemi di attività sono disgiunti
	all a: Attivita | a in attivitaObblig implies (
		a.cittaFruiz = destinazione and a not in attivitaOpzCompat  and
		/*le date sono compatibili*/ 
		all dp : Data | dp in datePartenzaPossibili implies
			a.dataInizioDisp.timestamp <= dp.timestamp and
			a.dataFineDisp.timestamp >= dp.timestamp+durata
	)

	//Tutte le attività compatibili sono o obbligatorie o opzionali
	all a : Attivita | a.cittaFruiz = destinazione implies a in (attivitaOpzCompat + attivitaObblig)
}

sig PacchettoAcquistato {
	originante : PacchettoPreconfigurato, // Pacchetto preconfigurato utilizzato come base 
															  // per la personalizzazione
	viaggioAndata: one Trasporto,
	viaggioRitorno: one Trasporto,
	soggiorno: one Soggiorno,
	dataPartenza: one Data,
	proprietario: one Cliente,
	
	attivitaAcquistate: set Attivita,
	giftList: set Attivita,
	pagamenti: some Pagamento
} {
	// Viaggio di andata, viaggio di ritorno e soggiorno sono fra quelli compatibili con il
	// il pacchetto originante
	viaggioAndata in originante.viaggiAndataCompat
	viaggioRitorno in originante.viaggiRitornoCompat
	soggiorno in originante.soggiorniCompat

	// Compatibilità delle attività per quanto riguarda le date
	all a : Attivita | a in attivitaAcquistate implies a in 
		originante.attivitaOpzCompat+originante.attivitaObblig and 
		a.dataInizioDisp.timestamp <= dataPartenza.timestamp and
		a.dataFineDisp.timestamp >= dataPartenza.timestamp + originante.durata
	
	// Tutte le attività obbligatorie sono acquistate
	all a : Attivita | a in originante.attivitaObblig implies a in attivitaAcquistate

	// Esiste esattamente un pagamento che contiene i viaggi e il soggiorno
	// (che è il pagamento dell'acquisto del pacchetto) ed esso è effettuato dal proprietario
	one p : Pagamento | 
		p in pagamenti and 
		viaggioAndata in p.prodottiAcquistati and 
		viaggioRitorno in p.prodottiAcquistati and
		soggiorno in p.prodottiAcquistati and p.clientePagante = proprietario
	
	//Tutte le attività acquistate sono in qualche pagamento (esattamente un pagamento)
	all a : Attivita | a in attivitaAcquistate implies one p : Pagamento | p in pagamenti and
		a in p.prodottiAcquistati

	//Solo le attività effettivamente in un pagamento sono attività acquistate 
	all a : Attivita | a in pagamenti.prodottiAcquistati implies a in attivitaAcquistate

	//Un'attività acquistata non può essere anche nella giftList
	all a: Attivita | a in attivitaAcquistate implies a not in giftList
}

abstract sig ProdottoBase {
	nome: one Stringa,
	descrizione: one Stringa
}

sig Trasporto extends ProdottoBase {
	cittaPartenza: one  Citta,
	cittaArrivo: one Citta,
	tipo: one Stringa
} {
	cittaPartenza != cittaArrivo
}

sig Soggiorno extends ProdottoBase {
	tipo: one Stringa,
	citta: one Citta
}

sig Attivita extends ProdottoBase {
	dataInizioDisp: one Data,
	dataFineDisp: one Data,
	prezzoAttiv: one Int,
	cittaFruiz: one Citta
} {
	dataFineDisp.timestamp > dataInizioDisp.timestamp
	prezzoAttiv >0
}

abstract sig UtenteRegistrato {
	userId: one Stringa,
	passwd: one Stringa,
	nome: one Stringa,
	cognome: one Stringa,
	email: one Stringa,
	dataNascita: one Stringa
}


sig Cliente extends UtenteRegistrato {
	codiceFiscale: one Stringa
}

sig Impiegato extends UtenteRegistrato {
}

one sig Admin extends UtenteRegistrato {
}

sig Pagamento {
	clientePagante: one Cliente,
	prodottiAcquistati: some ProdottoBase
}

//---------------------------------------------------------
//        DEFINIZIONE FATTI
//---------------------------------------------------------

// Due date diverse hanno timestamp diverso
fact noSameTimestamp {
	no disj d1, d2 : Data | d1.timestamp = d2.timestamp
}

// Non esistono due utenti con stesso UserID
fact userIdUnico {
	no disj u1, u2 : UtenteRegistrato | u1.userId = u2.userId
}

// Un pagamento deve avere prodotti al suo interno che appartengono
// solo al pacchetto a cui è associato
fact PagamentiDiUnSoloProdotto {
	all pa : PacchettoAcquistato,  p : Pagamento | p in pa.pagamenti implies
		p.prodottiAcquistati in 
			pa.(attivitaAcquistate + viaggioAndata + viaggioRitorno + soggiorno)
}

// Ogni pagamento contenuto in un P.A. è relativo ad un diverso prodotto
// fra quelli acquistati nel P.A.
fact pagamentoDiversiProdotti{
	no disj p1, p2 : Pagamento, pb : ProdottoBase, pa : PacchettoAcquistato |
		p1 in pa.pagamenti and p2 in pa.pagamenti and
		pb in p1.prodottiAcquistati and
		pb in p2.prodottiAcquistati 
}

// Un Pagamento non può essere legato a più P.A.
fact pagamentoNonCondiviso{
	no disj pa1, pa2 : PacchettoAcquistato, p : Pagamento | p in pa1.pagamenti and
		p in pa2.pagamenti
}

// Non esistono pagamenti non legati a P.A.
fact noPagamentiPerNulla{
	all p : Pagamento | one pa : PacchettoAcquistato | p in pa.pagamenti
}

//---------------------------------------------------------
//        DEFINIZIONE ASSERZIONI
//---------------------------------------------------------

// Non ci sono pagamenti che abbiano attività di altri pacchetti oltre a quello a cui sono associati
assert PagamentiFuoriPacchetto {
	no pa : PacchettoAcquistato, p : Pagamento | p in pa.pagamenti and
		p.prodottiAcquistati not in 
		pa.(attivitaAcquistate + viaggioAndata + viaggioRitorno + soggiorno)
}

// Non essitono attività sia nella GL che negli acquisti dello stesso P.A.
assert StessaAttivitaGLEAcquisti {
	no pa : PacchettoAcquistato, a : Attivita | a in pa.giftList and a in pa.attivitaAcquistate
}

// In un P.A. non ci sono attività in una città diversa da quella di destinazione
assert AttivitaCittaDiversa {
	no pa : PacchettoAcquistato, a : Attivita | a.cittaFruiz != pa.originante.destinazione and
		pa.attivitaAcquistate = a
}

// Ogni pacchetto acquistato ha almeno un pagamento
assert AlmenoUnPagamento {
	all pa : PacchettoAcquistato | #pa.pagamenti > 0
}

//---------------------------------------------------------
//        DEFINIZIONE PREDICATI
//---------------------------------------------------------

// Predicato per l'acquisto di un pacchetto e inserimento in giftlist
pred AcquistoDiUnPacchetto(p : Pagamento, pp : PacchettoPreconfigurato, 
		pa : PacchettoAcquistato, c : Cliente) {
	p.clientePagante = c and pa.originante = pp and pa.pagamenti = p
	#pa.attivitaAcquistate>0 and #pa.giftList > 0 
	pa.attivitaAcquistate + pa.viaggioAndata + pa.viaggioRitorno + pa.soggiorno = 
		pa.pagamenti.prodottiAcquistati
} 

// Predicato per l'acquisto di un'attività in un pacchetto già acquistato e rimozione dalla
// relativa gift list
pred AcquistoAttivitaPacchettoGiaComprato(pa, pa' : PacchettoAcquistato, a : Attivita) { 
	pa'.attivitaAcquistate = pa.attivitaAcquistate + a
	pa'.giftList = pa.giftList - a
	
	//Il resto rimane invariato
	pa'.originante = pa.originante
	pa'.viaggioAndata = pa.viaggioAndata
	pa'.viaggioRitorno = pa.viaggioRitorno
	pa'.soggiorno = pa.soggiorno
	pa'.dataPartenza = pa.dataPartenza
	pa'.pagamenti = pa.pagamenti
	pa'.proprietario = pa.proprietario
}

//Predicato per l'aggiunta di un'attività nella GL di un pacchetto già acquistato
pred AggiuntaAttivitaGiftListPacchettoGiaComprato(pa, pa' : PacchettoAcquistato, a : Attivita) {
	// Viene aggiunta l'attività alla gift list
	pa'.giftList = pa.giftList + a
	
	//Il resto rimane invariato
	pa'.originante = pa.originante
	pa'.viaggioAndata = pa.viaggioAndata
	pa'.viaggioRitorno = pa.viaggioRitorno
	pa'.soggiorno = pa.soggiorno
	pa'.dataPartenza = pa.dataPartenza
	pa'.pagamenti = pa.pagamenti
	pa'.attivitaAcquistate = pa.attivitaAcquistate
	pa'.proprietario = pa.proprietario
}

pred AcquistoPacchettoSuggeritoDaAmico(disj pa1, pa2 : PacchettoAcquistato, 
	disj c1, c2 : Cliente) {
	// pa1 appartiene a c1
	pa1.proprietario = c1
	
	// pa2 appartiene a c2, che è l'amico a cui c1 ha suggerito il pacchetto
	pa2.proprietario = c2
	
	// pa2 ha stessi trasporti, attività e soggiorno di pa1, parte lo stesso giorno
	// e ha lo stesso pacchetto originante
	pa2.attivitaAcquistate = pa1.attivitaAcquistate and
	pa2.soggiorno = pa1.soggiorno and
	pa2.viaggioAndata = pa1.viaggioAndata and
	pa2.viaggioRitorno = pa1.viaggioRitorno and
	pa2.dataPartenza = pa1.dataPartenza and
	pa2.originante = pa1.originante

	// pa2 ha un solo pagamento, fatto da c2, che è il pagamento di acquisto. 
	// In quel pagamento c'è tutto.
	#pa2.pagamenti = 1 and
	pa2.pagamenti.clientePagante = c2 and
	pa2.pagamenti.prodottiAcquistati = pa2.viaggioAndata + pa2.viaggioRitorno +
		pa2.soggiorno + pa2.attivitaAcquistate
}

//Predicato per la visualizzazione di un mondo completo
pred show() {}

//---------------------------------------------------------
//        COMANDI DI ESECUZIONE
//---------------------------------------------------------

check PagamentiFuoriPacchetto for 10
check StessaAttivitaGLEAcquisti for 10
check AttivitaCittaDiversa for 10
check AlmenoUnPagamento for 10

run AcquistoDiUnPacchetto for 5 but exactly 1 Pagamento ,exactly 1 PacchettoAcquistato, 
exactly 1 Cliente, exactly 1 PacchettoPreconfigurato
run AcquistoPacchettoSuggeritoDaAmico for 10
run AggiuntaAttivitaGiftListPacchettoGiaComprato for 10
run AcquistoAttivitaPacchettoGiaComprato for 5
run show for 12 but exactly 1 PacchettoAcquistato
